include "arithmetics/nat.ma".
include "basics/bool.ma".
include "basics/types.ma".
include "basics/deqsets.ma".


inductive Atom: Type[0] ≝
   Unit  : Atom
 | Name  : nat → Atom
 | CoName: nat → Atom .

(* Unit: notation and interpretation *)
interpretation "Unit" 'Unit = Unit.
notation "𝟙" with precedence 90 for @{ 'Unit }.

(* Atom: notation and interpretation *)
interpretation "Name" 'Name n = (Name n).
notation "hvbox(𝔸 \sub n)" with precedence 90 for @{ 'Name $n }.

(* Negative atom: notation and interpretation *)
notation "hvbox(𝔹 \sub n)" with precedence 90 for @{ 'CoName $n }.
interpretation "CoName" 'CoName n = (CoName n).

(* Atom sets *)

definition Atomeqb ≝ λa,b:Atom.
  match a with 
  [ Unit     ⇒ match b with 
               [ Unit  ⇒ true
               | _     ⇒ false]
  | Name   n ⇒ match b with 
               [ Name   m ⇒ (eqb n m)
               | _      ⇒ false]
  | CoName n ⇒ match b with 
               [ CoName m ⇒ (eqb n m)
               | _        ⇒ false]].
               
notation < "a == b" non associative with precedence 45 for @{Atomeqb $a $b }.

(* lemma ll: 
∀n1,n2.(𝔸 \sub n2) = (𝔸 \sub n1) → eqb n2 n1=true.
#H1 #H2 #H3 elim H1 elim H2 normalize /2/ *)

lemma Atomeqb_true: ∀a,b. iff (Atomeqb a b = true) (a = b).
#a elim a
[1: #b cases b 
 [1:/2/ (* Ho guardato la dimostrazione 
           del lemma beqitem_true in chapter7.ma
           del tutorial. *)
 |2,3: #N % normalize #H destruct ]
|2:#X #b cases b [ |#Y |#Y ] 
   % normalize #H destruct 
|3: #X #b cases b [ |#Y |#Y] 
   % normalize #H destruct ]
   [1,3: (* applico 
      theorem eqb_true_to_eq: 
         ∀n,m:nat. eqb n m = true → n = m.
      in rithmetics/nat.ma *)
     lapply (eqb_true_to_eq X Y H) #Heq >Heq @refl
     (* applico 
        theorem eqb_n_n: ∀n. eqb n n = true.
        in rithmetics/nat.ma *)
   |2,4: @(eqb_n_n Y)  ]   
qed.


definition AtomSet ≝ mk_DeqSet Atom Atomeqb Atomeqb_true.

definition DeqBool ≝ mk_DeqSet bool beqb beqb_true



inductive Unit: Prop ≝  
mkUnit : Unit.

(* Par *)
inductive Par (A,B:Prop) : Prop ≝
    mkPar : A → B → Par A B.

(* Seq *)
inductive Seq (A,B:Prop) : Prop ≝
    mkSeq : A → B → Seq A B.

(* CoP *)
inductive CoP (A,B:Prop) : Prop ≝
    mkCoP : A → B → CoP A B.




inductive Not (A:Prop): Prop ≝
nmk: (A → False) → Not A.

interpretation "logical not" 'not x = (Not x).




definition name   ≝ λA:Type[0].λx,a:A.〈 x=a, true 〉.
interpretation "name" 'name x = (name ? x).
notation "x+" with precedence 100 for @{name $x}.  
definition coname ≝ λA:Type[0].λx,a:A.〈 x=a, false 〉.
interpretation "singleton" 'coname x = (coname ? x).
notation "x-" with precedence 100 for @{coname $x}.

(* check name.   *)

definition a_a ≝ name nat 1. definition a_b ≝ name nat 2.
definition a_c ≝ name nat 3. definition a_d ≝ name nat 4.
definition ca_a ≝ coname nat 1. definition ca_b ≝ coname nat 2.
definition ca_c ≝ coname nat 3. definition ca_d ≝ coname nat 4.



inductive operator : Type[0] ≝
  mkpar : operator
| mkcopar : operator
| mkseq : operator.  

definition par_base (A:Type[0]) (P:A→Prop×bool) (Q:A→Prop×bool) ≝ 
 λ a:A. 
  match \snd (P a)  with
  [ false ⇒ false
  | cons a tl ⇒ (x == a) ∨ memb S x tl
  ].


let rec memb (S:DeqSet) (x:S) (l: list S) on l  ≝
  match l with
  [ nil ⇒ false
  | cons a tl ⇒ (x == a) ∨ memb S x tl
  ].



λA,P,Q,a.P a ∨ Q a.
interpretation "union" 'union a b = (union ? a b).




